T:Type, L:T List, i, j:||L||. ||swap(L;i;j)|| = ||L||   

latex

Definitions	t  T, x:A. B(x), ||as||, {i..j}, P  Q, False, A, P & Q, AB, i  j < k, , (i, j), swap(L;i;j)
Lemmas	permute list length, flip wf, le wf, int seg wf, length wf1